package scala.examples.tcpoly.calculi.stlc

import scala.examples.tcpoly.binding.frescala._

trait Syntax extends Binding with BindingSyntax with Substitution  { self: MyAbsM with Syntax =>
  import AM.result
  
  sealed abstract class Term extends Nominal[Term] with CheckingEquality[Term] {
    def isValue: Boolean    
    def ===(o: Term) = (this, o) match {
      case ( _ , x: MetaTerm) => x === this // delegate to MetaTerm
      case (V(n) , V(n2) ) => n == n2
      case (L(t, b) , L(t2, b2) ) => t === t2 && b === b2
      case (A(a, b), A(a2, b2) ) => a === a2 && b === b2
      case (T, T) => true
      case (F, F) => true
      case _ => false
    }    
  }

  case object T extends Term {
    def isValue = true
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true
    def supp = Nil
  }
 
  case object F extends Term {
    def isValue = true
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true
    def supp = Nil
  }  
  
  case class V(n: Name) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = V(n swap(a, b))
    def fresh(a: Name) = n.fresh(a)
    def supp = n.supp
  }  

  case class L(tp: Type, body: \\[Term]) extends Term {
    def isValue = true

    def swap(a: Name, b: Name) = L(tp swap(a,b), body swap(a, b))
    def fresh(a: Name) = tp.fresh(a) && body.fresh(a)
    def supp = tp.supp ::: body.supp  
  }
  
  case class A(fun: Term, arg: Term) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = A(fun swap(a, b), arg swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
    def supp = fun.supp ::: arg.supp
  }  

  def absTm[T <% Substable[Term, T]](abs: \\[T]): Substable[Term, \\[T]] = new AbsSubstTo[Term].AbsIsSubstable(abs)

  implicit def TermSubstTerm(self: Term): Substable[Term, Term] = new Substable[Term, Term] { 
    def subst(sub: Name => Option[Term]): AM[Term] = self match {
      case V(n) => AM.result(sub(n).getOrElse[Term](self))
      case L(tp, b) => for(tp2 <- tp subst(sub); b2 <- absTm(b) subst(sub)) yield L(tp2, b2)
      case A(f, a) => for(f2 <- f subst(sub); a2 <- a subst(sub)) yield A(f2, a2)
      case T => result(T)
      case F => result(F)
    }
  }
  
  // term variable used by the type checker
  case class MetaTerm(override val isValue: Boolean, override val tag: Tag, override val name: String, override var v: Option[Term]) extends Term with MetaVar[Term] {
    def unifies(o: Term) = Some(o)
  }  
    
  import AM.{result, fail}
  def isVar(x: Any): AM[(Name)] = x match { case V(n) => result((n)) case _ => fail("expected Var") }
  def isLam(x: Any): AM[(Type, \\[Term])] = x match { case L(t, b) => result((t, b)) case _ => fail("expected Lam") }
  def isApp(x: Any): AM[(Term, Term)] = x match { case A(a,b) => result((a,b)) case _ => fail("expected App") }  
  def isTrue(x: Any): AM[Unit] = x match { case T => result(()) case _ => fail("expected True") }
  def isFalse(x: Any): AM[Unit] = x match { case F => result(()) case _ => fail("expected False") }
  
  
  sealed abstract class Type extends Nominal[Type] with CheckingEquality[Type] {
    def ===(o: Type) = (this, o) match {
      case ( _ , x: MetaType) => x === this // delegate to MetaType
      case (Arr(f, t) , Arr(f2, t2) ) => f === f2 && t === t2
      case (TBool, TBool) => true
      case _ => false
    }    
  }  
  
  case class Arr(from: Type, to: Type) extends Type {
    def swap(a: Name, b: Name) = Arr(from swap(a, b), to swap(a, b))
    def fresh(a: Name) = from.fresh(a) && to.fresh(a)
    def supp = from.supp ::: to.supp
  }
  
  case object TBool extends Type {
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true
    def supp = Nil
  }  

  implicit def TypeSubstTerm(self: Type): Substable[Term, Type] = new Substable[Term, Type] { 
    def subst(sub: Name => Option[Term]): AM[Type] = self match {
      case Arr(f, a) => for(f2 <- f subst(sub); a2 <- a subst(sub)) yield Arr(f2, a2)
      case TBool => result(TBool)
    }
  }
  
  
  // type variable used by the type checker
  case class MetaType(override val tag: Tag, override val name: String, override var v: Option[Type]) extends Type with MetaVar[Type] {
    def unifies(o: Type) = Some(o)
  }  
  
  def isArr(x: Any): AM[(Type, Type)] = x match { case Arr(f, t) => result((f, t)) case _ => fail("expected Arr") }
  
  
  
}